Rename `linux' to `gnu_linux'.
authorRichard Stallman <rms@gnu.org>
Sun, 2 Oct 2011 22:43:52 +0000 (18:43 -0400)
committerRichard Stallman <rms@gnu.org>
Sun, 2 Oct 2011 22:43:52 +0000 (18:43 -0400)
commit95c4cbc41f53f7cb8838d8c33aa2c353f496803e
treef305902690bf856f327ad399daad1a580b480c9e
parente0e4fc00cfb931cc61eab7687d787b337faa4d7e
Rename `linux' to `gnu_linux'.
ChangeLog
configure.in